00100	INF_OP: *,o,∪,∩,-;
00200	PRE_OP:G,K,e,f,↑,g,h,m;
00300	INF_PRED:↔,⊂,ε,=;
00350	PRE_PRED:s;
00400	EQUALITY:=;
00500	VAR: x,y,z,u,v,X,Y,Z,U,V;
00600	a1:x*(y*z)=(x*y)*z;
00700	a2:x=y ≡x*z =x*y;
00800	a3:x=y≡z*x=z*y;
00900	a6: x*e=x;
01000	a7:e*x=x;
01100	a8:x*↑(x)=e;
01200	a9:↑(x)*x =e;
01300	a10:↑(↑(x))=e;
01400	a11:(f(x,y)εx⊃f(x,y)εy)⊃x⊂y;
01500	a12:x⊂y ⊃(zεx ⊃z εy);
01600	a13:(zεx ∨ zεy) ⊃zε(x∪y);
01700	a14:zε(x∪y)⊃(zεx ∨zεy);
01800	a15:(zεx∧zεy)⊃zεx∩y;
01900	a16:zεx∩y ⊃(zεx∧zεy);
02000	a17:(zεx∧¬(zεy))⊃zεx-y;
02100	a18:zεx-y⊃(zεx∧¬(zεy));
02200	a19:(x⊂y∧y⊂x)≡ x↔y;
02300	a21:(((g(x)εx∧h(x)εx)⊃g(x)*h(x)εx)∧(g(x)εx ⊃↑(g(x))εx))⊃s(x);
02400	a22:s(z)⊃(eεz∧(xεz⊃↑(x)εz)∧(↑(x)εz⊃xεz));
02500	a23:s(z)⊃(x*yεz ∨¬xεz ∨ ¬yεz);
02600	a24:s(K);
02700	a25:xεK o z ⊃(x=m(x,z)*z ∧m(x,z)εK);
02800	a26:x*z εK o z∨¬xεK;
02900	THEOREM:(K o G ↔ K ≡ GεK);